$\forall$$M_{1}$, $M_{2}$:MsgA. $M_{1}$ $\subseteq$ $M_{2}$ $\Rightarrow$ ($\forall$$k$:Knd, $x$:Id. $M_{2}$.rframe($k$ reads $x$) $\Rightarrow$ $M_{1}$.rframe($k$ reads $x$))